Nuprl Lemma : es-prior-interface-locl
11,40
postcript
pdf
es
:ES,
X
:AbsInterface(Top),
e
:E. (
(
e
prior(
X
)))
(prior(
X
)(
e
) <loc
e
)
latex
Definitions
b
,
(
e
<loc
e'
)
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
ES
,
AbsInterface(
A
)
,
E
,
x
:
A
B
(
x
)
,
P
&
Q
,
P
Q
,
e
X
,
A
,
prior(
X
)
,
X
(
e
)
,
Top
Lemmas
es-prior-interface-val
,
event
system
wf
,
top
wf
,
es-interface
wf
,
es-E
wf
,
es-locl
wf
,
assert
wf
origin
es:ES, X:AbsInterface(Top), e:E. (
(e 
prior(X))) 
(prior(X)(e) <loc e) es:ES, X:AbsInterface(Top), e:E. ((e prior(X))) (prior(X)(e) <loc e) b
B(x)x:A. B(x)
B(x) Q X
A